Associativity of Join, and lots more #1768
Conversation
…c; add equiv_homotopic_inverse
jdchristensen
requested review from
Alizter,
JasonGross,
mikeshulman and
jarlg
|
I should have mentioned that the real meat is in the 9th commit ("Join/Core: recursion equivalence for join; join_sym via Yoneda") and the two commits near the end ("Join/TriJoin: 3 variable induction/recursion principles" and "Join/JoinAssoc: associativity of Join using Yoneda lemma"). Those three can be reviewed as a unit. |
jdchristensen
force-pushed
the
join-assoc
branch
from
e68da51
to
692dd46
Compare
|
I've remembered why we use Cubical in the Torus proof now, and its solely for managing the path algebra that crops up. To demonstrate how tricky things are, I don't know of anybody who has written our the induction principle for the torus in full using only paths. In contrast, the use of cubical constructions actually allows us to write an induction principle down and also reason about it in a straightforward way. My last 3x3 lemma attempt (which is attempt no. 6 for me) used something similar to what you have here, although I didn't have the ZeroGpd version of yoneda hence I was getting bogged down by funext and trying to write down the higher paths for "pushout algebras". I'm glad to see this can actually pull through! I tried to take your ideas and apply them to the Torus being equivalent to the produce of circles. This is actually quite different from the join, since we don't have so much symmetry to exploit. In the join case, and probably many others, we can use the twist and swap maps that you defined to get places. When it comes to the Torus, you still have to prove: I even tried defining Anyway, the take away from this is that this technique has some limitations, but overall is a much cleaner and practical way than anything that has come before! I look forward to the results about pushouts and smash products. When this is merged, I'll PR my experiments with the torus so they can be looked at. It might be that I've missed something. |
I'm not necessarily planning to do these myself... By the way, one of the tricks hidden in the formalization is the use Mike's notion of an injective and essentially surjective map of 0-groupoids, instead of directly proving that there is a bi-invertible map of 0-groupoids. I originally did it as a bi-invertible map, and it's fine, but I was able to delete 10 or 20 lines by using Mike's notion. I never have to prove that |
I didn't mean that you would! Just that it is clearer how to go about them now. |
|
Does anyone want to look at this more before it is merged? I'm happy to wait if someone speaks up, but will merge Tuesday if I don't hear anything. |
There was a problem hiding this comment.
Overall looks very good to me. I like these new tacticals we have now. Have you got any corollaries of join associativity that you want to prove now? Joins of spheres and the Hopf fibrartion (if this is still the state-of-the-art) are some that come to mind. If not, I might look into carrying them out soon.
It would be nice if you could fill in lemma 8.5.9 of the HoTT book with join assoc too.
|
This sounds really neat! Unfortunately I don't have time to look at it right now, and probably won't for a while, so you shouldn't wait on me. |
There is no 8.5.9 in contrib/HoTTBook.v, probably because that lemma in the HoTT book doesn't have a label. Maybe someone else can fix this? |
@Alizter My use of associativity will be for some WIP, so feel free to tackle other things! I'd certainly find it handy to know that joins of spheres are spheres, and to have the Hopf construction available. |
|
@jdchristensen I'll make a note of the missing label and try fixing it soon. It might be fixed upstream just that we need to run the hott book scripts again. Excellent, I'll post my WIP torus PR at some point, and also have a stab at joining spheres. |
|
@Alizter I looked in the book source, and there is no \label. |
|
@jdchristensen I opened an issue. |
|
@Alizter About spheres, I think the main ingredient is showing that |
This is a big PR, so I'll leave it open for a while and would appreciate it if a few people could help review it. It's best to review the commits independently, and maybe people can help by reviewing a subset of the commits. Maybe @JasonGross could take a look at the 11th commit, "Add refine_lhs family of tactics, and demo usage"?
The first two commits don't need review, as they just move Join.v to Join/Core.v and add the meta-file Join.v.
The goal is to prove the associativity of Join, but along the way, many other changes were made. For the associativity, the idea is to use the Yoneda lemma for 0-groupoid-valued functors. This leads to a long argument, because of the need to set up the wild category structures, but it has the advantage that each piece is reasonably straightforward. For most pieces, the top cell can be handled by induction, and for the remaining two or three, the path algebra is not bad. It's long-winded, but every direct approach I tried got bogged down in path algebra, with no obvious way to do induction.
I also set up the same framework in the two-variable case and use it to prove symmetry of the join, even though that has a direct proof. I think this provides a good model for future work using this technique. For example, the ideas here should also work for the 3x3 lemma, the associativity of smash, and similar tasks.
I checked the timing. The single-threaded build takes ~1.5s longer, and the two new files take about 1.5s, so that makes sense. No existing file changed significantly in speed. The
-j8build speed is unchanged.